The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m)

Rewrite Strategy: FULL

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m)

S is empty.
Rewrite Strategy: FULL

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
cons/0
map_f/0
f/0
f/1

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

S is empty.
Rewrite Strategy: FULL

(5) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
fstsplit(s(n), cons(t)) →⁺ cons(fstsplit(n, t))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [n / s(n), t / cons(t)].
The result substitution is [ ].

(6) BOUNDS(n^1, INF)